Nuprl Definition : R-consistent 0,22
Consistent(R;es)
== case R of 
== Rnone => True
== Rplus(left,right)=>rec1,rec2.rec1 & rec2
== Rinit(i,T,x,v)=> @i x initially v:T
== Rframe(i,T,x,L)=> @i only events in L change   x : T
== Rsframe(l,tg,L)=> only events in L send on l with tg
== Reffect(i,ds,k,T,x,f)=> @i events of kind k change x to f State(ds) (val:T)
== Rsends(ds,k,T,l,dt,g)=> sends k(v:T) on l:
== Rsends(ds,k,T,l,dt,g)=> tagged(g,State(ds),v):dt
== Rpre(i,ds,a,T,P)=> @i Precondition for a(v)
== Rpre(i,ds,a,T,P)=> @i P State(ds) (v:T)
== Raframe(i,k,L)=> @i: k affects only L
== Rbframe(i,k,L)=> @i:k sends only on links in L
== Rrframe(i,x,L)=> @i: only members of L read x 
latex

clarification:

Consistent(R;es)
== case R of 
== Rnone => True
== Rplus(left,right)=>rec1,rec2.rec1 & rec2
== Rinit(i,T,x,v)=> init-p(es; i; T; x; v)
== Rframe(i,T,x,L)=> frame-p(es; i; T; x; L)
== Rsframe(l,tg,L)=> sframe-p(es;l;tg;L)
== Reffect(i,ds,k,T,x,f)=> effect-p(es;i;ds;k;T;x;f)
== Rsends(ds,k,T,l,dt,g)=> sends-p(es;ds;k;T;l;dt;g)
== Rpre(i,ds,a,T,P)=> pre-p(es;i;ds;a;T;P)
== Raframe(i,k,L)=> aframe-p(es;i;k;L)
== Rbframe(i,k,L)=> bframe-p(es;i;k;L)
== Rrframe(i,x,L)=> rframe-p(es;i;x;L) 
latex

Definitionses realizer ind, True, P & Q, @i x initially v:T, @i only events in L change   x : T, only events in L send on l with tg, @i events of kind k change x to f State(ds) (val:T), sends k(v:T) on l:tagged(g,State(ds),v):dt, @i Precondition for a(v)P State(ds) (v:T), @i: k affects only L, @i:k sends only on links in L, @i: only members of L read x
FDL editor aliasesR-consistent

origin